perm filename NUMBER.AX[W76,JMC] blob sn#198572 filedate 1976-01-28 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE OPCONST INTERVAL(NATNUM,NATNUM) ε SET
C00003 ENDMK
C⊗;
DECLARE OPCONST INTERVAL(NATNUM,NATNUM) ε SET;
AXIOM EVEN:	EVEN(0),
		∀m.(EVEN(m) ≡ ¬EVEN(SUCC(m)));;